Nuprl Lemma : l_before_sublist
11,40
postcript
pdf
T
:Type,
L1
,
L2
:(
T
List).
L1
L2
{
x
,
y
:
T
.
x
before
y
L1
x
before
y
L2
}
latex
ProofTree
Definitions
t
T
,
x
before
y
l
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
sublist
wf
,
sublist
transitivity
origin
T:Type, L1, L2:(T List). L1 
L2 
{x, y:T. x before y 
L1 x before y L2}
T:Type, L1, L2:(T List). L1 L2 {x, y:T. x before y L1 x before y L2}
T l Qx:A. B(x)